/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transl;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.List;

import alloy.bool.BooleanFormula;
import alloy.bool.PartialAssignment;
import alloy.util.Dbg;

/**
 * Translation of an {@linkplain alloy.ast.IntExpr integer-valued node}.
 */
public class IntTransl extends Transl {
    /**
     * Bits representing a binary number, where each bit is
     * a boolean formula.  bits[0] is the lowest-order bit.
     * bit number length is not fixed: different IntTransls
     * can have different bit lengths.  If {@link #_isTwosComplement}
     * is true then the highest bit in {@link #_bits} represents
     * a negative power of two, otherwise it represents a positive
     * power of two; all other bits always represent a positive
     * power of two.
     * @see #interpretAsInt
     */
    private BooleanFormula[] _bits;

    /**
     * Is this is a two's-complement representation?  If yes,
     * the meaning of the higher-order bit of {@link #_bits} is
     * (-2^{_bits.length}) rather than 2^{_bits.length}.
     */
    private boolean _isTwosComplement;

    ///////////////////////////////////

    public static final IntTransl ZERO = new IntTransl(new BooleanFormula[]{});
    public static final IntTransl ONE = new IntTransl(new BooleanFormula[]{BooleanFormula.TRUE()});
    public static final IntTransl TWO = new IntTransl(new BooleanFormula[]{BooleanFormula.FALSE(),
									   BooleanFormula.TRUE()});

    /**
     * Construct an IntTransl representing a non-negative integer.
     */
    public IntTransl(BooleanFormula[] bits_) { this._bits = bits_; }

    /**
     * Construct an IntTransl representing an integer in two's complement notation,
     * if the second argument is true.
     */
    public IntTransl(BooleanFormula[] bits_, boolean isTwosComplement_) {
	this._bits = bits_;
	_isTwosComplement = isTwosComplement_;
    }

    /** Return the number of bits in the representation of this integer. */
    public int size() { return _bits.length; }

    /**
     * Is this a two's complement representation?  If not, all bits represent
     * positive powers of two.  If it is, the highest-order bit represents
     * a negative power of two.
     */
    public boolean isTwosComplement() { return _isTwosComplement; }

    /**
     * Return the {@link BooleanFormula} representing the given bit of the integer.
     * Remember that if {@link #isTwosComplement} then the highest-order bit
     * (the one with index equal to {@link #size}-1) represents a negative
     * power of two.
     */
    public BooleanFormula getBit(int i_) {
	Dbg.chk(!_isTwosComplement || i_ < size());
	return i_ < size() ? _bits[i_] : BooleanFormula.FALSE();
    }

    /**
     * Return the array of Boolean formulas for each bit of the translation.
     * Used internally by {@link TranslVisitor}.
     */
    BooleanFormula[] getBits() { return _bits; }

    /**
     * Construct an IntTransl that represents the same integer as this IntTransl,
     * but in two's complement representation of the given size.  Precondition:
     * that the given size be sufficient to represent this integer in two's complement.
     */
    IntTransl computeSignExtension(int size_) {
	//System.out.println("sign-extending " + this);
	if (_isTwosComplement && size_ == _bits.length) {
	    //System.out.println("nothing to do.");
	    return this;
	}
	Dbg.chk(size_ > _bits.length);
	BooleanFormula[] newBits = new BooleanFormula[size_];
	System.arraycopy(_bits, 0, newBits, 0, _bits.length);
	BooleanFormula fillValue = _isTwosComplement ? _bits[_bits.length-1] : BooleanFormula.FALSE();
	//System.out.println("compl=" + _isTwosComplement);
	//System.out.println("fillValue=" + fillValue);
	Arrays.fill(newBits, _bits.length, newBits.length,
		    fillValue);
	IntTransl r =  new IntTransl(newBits, true /* is two's complement */);
	//System.out.println("got " + r);
	return r;
    }

    /** Compute the negation of this IntTransl */
    IntTransl computeNegation() {
	IntTransl t = _isTwosComplement ? this : computeSignExtension(_bits.length + 1);
	//System.out.println("after ext: " + t);
	    
	BooleanFormula[] onesComplement = new BooleanFormula[t._bits.length];
	for (int i=0; i<t._bits.length; i++)
	    onesComplement[i] = t._bits[i].not();
	IntTransl onesComplementPlusOne = _constructAdder(new IntTransl(onesComplement),
							  ONE);
	return new IntTransl(_trim(onesComplementPlusOne._bits, onesComplement.length), true /* isTwosComplement */);
    }

    /** Trim the given BooleanFormula[] to the specified length (i.e. return a new array if necessary) */
    private static BooleanFormula[] _trim(BooleanFormula[] bf_, int len_) {
	if (bf_.length > len_) {
	    BooleanFormula[] newBF = new BooleanFormula[len_];
	    System.arraycopy(bf_, 0, newBF, 0, len_);
	    return newBF;
	} else return bf_;
    }

    /**
     * Return the flat list of {@link BooleanFormula}s in this IntTransl. 
     */
    public List /* of BooleanFormula */ getBooleanFormulas() { return Collections.unmodifiableList(Arrays.asList(_bits)); }

    /**
     * Return a newly allocated IntTransl representing the number of tuples in the
     * given relation-valued expression.
     */
    public static IntTransl fromExprTransl(ExprTransl relTransl_) {
	// construct an adder to add d.scope one-bit binary numbers
	BooleanFormula[] bforms = (BooleanFormula[])relTransl_.getBooleanFormulas().toArray(new BooleanFormula[]{});
	return _fromExprTransl(bforms, 0, bforms.length);
    }
    
    /** Recursive helper for fromExprTransl: constructs a bit vector
	representing the sum of setBits[low] through setBits[hi-1]. */
    private static IntTransl _fromExprTransl(BooleanFormula[] setBits_,
					    int low_, int hi_)
    {
	int nbits = hi_ - low_;
	if (nbits < 1) return new IntTransl(new BooleanFormula[]{});
	if (nbits == 1) return new IntTransl(new BooleanFormula[]{setBits_[low_]});
	
	// else, split the bit set into lower and upper half,
	// recursively construct sums for the halves,
	// then construct a binary adder to add the two sums.
	int mid = (low_ + hi_) / 2;
	return _constructAdder(_fromExprTransl(setBits_, low_, mid),
			       _fromExprTransl(setBits_, mid, hi_));
    }

    /** construct a binary adder for two denotations: i.e. each denotation
	represents some binary number constructed from state bits,
	and we return a {@link IntTransl} representing a binary number
	which is the sum of the two binary numbers represented by the given denotations. */
    private static IntTransl _constructAdder(IntTransl d1_,
					     IntTransl d2_)
    {
	Dbg.chk((!d1_._isTwosComplement && !d2_._isTwosComplement) ||
		(d1_._isTwosComplement && d2_._isTwosComplement && d1_.size() == d2_.size()));
	int resultSize = Math.max(d1_.size(), d2_.size()) + 1;

	
	BooleanFormula[] result = new BooleanFormula[resultSize];
	BooleanFormula carry = BooleanFormula.FALSE();
	for (int i=0; i<resultSize; i++) {
	    BooleanFormula
		b1 = i==resultSize-1 ? BooleanFormula.FALSE() : d1_.getBit(i),
		b2 = i==resultSize-1 ? BooleanFormula.FALSE() : d2_.getBit(i);
	    BooleanFormula
		b1only = b1.and(b2.not()).and(carry.not()),
		b2only = b2.and(b1.not()).and(carry.not()),
		carryOnly = carry.and(b1.not()).and(b2.not()),
		all3 = b1.and(b2).and(carry);
	    result[i] = b1only.or(b2only).or(carryOnly).or(all3);
	    carry = b1.and(b2).or(b1.and(carry)).or(b2.and(carry));
	}
	Dbg.chk(carry == BooleanFormula.FALSE());
	return new IntTransl(result);
    }  // _constructAdder()

    /**
     * Construct an IntTransl representing the specified integer constant.
     */
    public static IntTransl fromIntConst(int constVal_) {
	// return a constant array
	//Dbg.chk(constVal_ >= 0, "can't deal with negative values (yet)");
	
	if (constVal_ == 0) return ZERO;
	if (constVal_ == 1) return ONE;
	
	// determine index of the highest "one" bit.
	BooleanFormula[] bits = new BooleanFormula[64];
	int absVal = Math.abs(constVal_);
	int last_1_bit = 0;
	long mask = 1;
	for (int i=0; i<bits.length && mask <= absVal; i++) {
	    boolean thisBit1 = ((absVal & mask) > 0);
	    if (thisBit1) last_1_bit = i;
	    bits[i] =  thisBit1 ? BooleanFormula.TRUE() : BooleanFormula.FALSE();
	    mask <<= 1;
	}

	// trim the trailing zero bits
	BooleanFormula[] nbits = new BooleanFormula[last_1_bit+1];
	for (int i=0; i<nbits.length; i++)
	    nbits[i] = bits[i];

	IntTransl result = new IntTransl(nbits);
	IntTransl r =  constVal_ > 0 ? result : result.computeNegation();
	//System.out.println("intconst: " + r);
	return r;
    }

    /**
     * Construct a formula that is true iff this IntTransl evaluates
     * to the same integer as the given IntTransl.
     */
    public FormulaTransl eq(IntTransl that_) {
	//System.out.println("inteq: " + this + " " + that_);
	BooleanFormula result = BooleanFormula.TRUE();

	IntTransl[] ints = _getUniformTransls(this, that_);
	//System.out.println("inteq unif: " + Arrays.asList(ints));
	
	List resultFormulas = new ArrayList();
	for (int i=0; i<ints[0]._bits.length; i++)
	    resultFormulas.add(ints[0]._bits[i].iff(ints[1]._bits[i]));
	
	return new FormulaTransl(BooleanFormula.makeAnd(resultFormulas));
    }

    /**
     * Construct a Boolean formula that is true iff this IntTransl evaluates
     * to an integer that is less than or equal to the integer to which that_
     * evaluates.
     */
    public FormulaTransl le(IntTransl that_) {
	//System.out.println("int le: " + this + " " + that_);
	IntTransl[] ints = _getUniformTransls(this, that_);
	//System.out.println("uniform: " + Arrays.asList(ints));
	
	BooleanFormula comparator = BooleanFormula.TRUE();
	BooleanFormula prevEqual = BooleanFormula.TRUE();
	int comparatorLen = ints[0].size() - 1;
	for (int i=comparatorLen; i>=0; i--) {
	    BooleanFormula origBit = ints[0].getBit(i);
	    BooleanFormula permBit = ints[1].getBit(i);
	    BooleanFormula thisOrdered =
		i == comparatorLen ? permBit.implies(origBit) : origBit.implies(permBit);

	    comparator = comparator.and(prevEqual.implies(thisOrdered));
	    prevEqual = prevEqual.and(origBit.iff(permBit));
	}  // loop over bits
	//System.out.println("comparator at end: " + comparator);
	return new FormulaTransl(comparator);
    }

    /**
     * Construct a formula that is true iff this IntTransl evaluates
     * to a different integer from the given IntTransl.
     */
    public FormulaTransl ne(IntTransl that_) {
	return (FormulaTransl)this.eq(that_).not();
    }
    
    /**
     * Construct a Boolean formula that is true iff this IntTransl evaluates
     * to an integer that is less than to the integer to which that_
     * evaluates.
     */
    public FormulaTransl lt(IntTransl that_) {
	return this.le(that_).and(this.ne(that_));
    }
    
    /**
     * Construct a Boolean formula that is true iff this IntTransl evaluates
     * to an integer that is greater than or equal to the integer to which that_
     * evaluates.
     */
    public FormulaTransl ge(IntTransl that_) {
	return (FormulaTransl)this.lt(that_).not();
    }
    
    /**
     * Construct a Boolean formula that is true iff this IntTransl evaluates
     * to an integer that is greater than the integer to which that_
     * evaluates.
     */
    public FormulaTransl gt(IntTransl that_) {
	return (FormulaTransl)this.le(that_).not();
    }

    /**
     * Given two IntTransls i1 and i2, compute IntTransls i1' and i2' which represent
     * the same integers as i1 and i2 respectively, but use two's complement representation
     * of the same width for both integers.  This makes it easier to specify
     * various operations on the integers.  i1' and i2' are returned in a newly allocated
     * two-element array.
     */
    private static IntTransl[] _getUniformTransls(IntTransl i1_, IntTransl i2_) {
	int newLen = Math.max(i1_._isTwosComplement ? i1_.size() : i1_.size() + 1,
			      i2_._isTwosComplement ? i2_.size() : i2_.size() + 1);
	newLen++;
	i1_ = i1_.computeSignExtension(newLen);
	i2_ = i2_.computeSignExtension(newLen);
	Dbg.chk(i1_._isTwosComplement && i2_._isTwosComplement && i1_.size() == i2_.size());
	return new IntTransl[]{i1_,i2_};
    }

    /**
     * Compute an IntTransl which always represents the integer that is the sum
     * of the integers represented by this and that_.
     */
    public IntTransl plus(IntTransl that_) {
	IntTransl i1 = this, i2 = that_;
	if (!_isTwosComplement && !that_._isTwosComplement)
	    return _constructAdder(i1, i2);

	IntTransl[] i = _getUniformTransls(i1,i2);

	//System.out.println("uniformTransls: " + Arrays.asList(i));
	IntTransl result = _constructAdder(i[0], i[1]);
	return new IntTransl(_trim(result._bits, i[0].size()), true /* two's complement */);
    }

    /**
     * Compute an IntTransl which always represents the integer that is the difference
     * of the integers represented by this and that_.
     */
    public IntTransl minus(IntTransl that_) { return this.plus(that_.computeNegation()); }

    /**
     * Compute an IntTransl which represents an integer equal to the sum of the integers
     * represented by the IntTransl's in the given list.
     */
    public static IntTransl makeSum(List /* of IntTransl */ intTransls_) {
	//System.out.println("makeSum: " + intTransls_);
	return makeSum((IntTransl[])intTransls_.toArray(new IntTransl[]{}));
    }
    
    /**
     * Compute an IntTransl which represents an integer equal to the sum of the integers
     * represented by the IntTransl's in the given array.
     */
    public static IntTransl makeSum(IntTransl[] intTransls_) {
	//System.out.println("makeSum: " + Arrays.asList(intTransls_));
	return _makeSum(intTransls_, 0, intTransls_.length);
    }

    /**
     * Compute an IntTransl which represents an integer equal to the sum of the integers
     * represented by the IntTransl's in the given sub-array.
     */
    private static IntTransl _makeSum(IntTransl[] intTransls_, int from_, int to_) {
	if (from_ >= to_) return ZERO;
	if (from_+1 == to_) return intTransls_[from_];
	int mid = (from_ + to_) / 2;
	return _makeSum(intTransls_, from_, mid).plus(_makeSum(intTransls_, mid, to_));
    }

    /**
     * Construct an IntTransl which represents the integer represented by thenTransl_ when
     * ifTransl_ is true, and represents the integer represented by elseTransl_ when
     * ifTransl_ is false.
     */
    public static IntTransl ifThenElse(FormulaTransl ifTransl_,
                                       IntTransl thenTransl_,
                                       IntTransl elseTransl_) {
	IntTransl[] ints = _getUniformTransls(thenTransl_,elseTransl_);

        BooleanFormula ifFormula = ifTransl_.formula;
        int resultSize = ints[0].size();

        BooleanFormula[] result = new BooleanFormula[resultSize];
        for (int i = 0; i < resultSize; i++) {
            BooleanFormula thenBit = ints[0].getBit(i);
            BooleanFormula elseBit = ints[1].getBit(i);
            result[i] = ifFormula.implies(thenBit).and(ifFormula.not().implies(elseBit));
        }
        return new IntTransl(result, true /* isTwosComplement */);
    }
            

    /**
     * Return a string containing the integer represented by this
     * IntTransl for the given setting of the Boolean variables.
     * @see #interpretAsInt
     */
    public String interpret (boolean [] assignment) {
	return String.valueOf(interpretAsInt(assignment));
    }

    /**
     * Return the integer represented by this IntTransl for
     * the given setting of Boolean variables.
     */
    public long interpretAsInt(boolean [] assignment) {
	long value = 0;
	long mask = 1;
	for (int i=0; i<_bits.length; i++) {
	    Dbg.chk(mask > 0);
	    if (_bits[i].interpret(assignment)) {
		if (i < _bits.length-1 || !_isTwosComplement)
		    value += mask;
		else
		    value -= mask;
	    }
	    mask <<= 1;
	}
	return value;
    }

    /**
     * Simplify all {@link BooleanFormula}s in this IntTransl with the given
     * partial assignment.
     */
    public void simplify(PartialAssignment pa_) {
	for (int i=0; i<_bits.length; i++)
	    _bits[i] = _bits[i].simplify(pa_);
    }

    /**
     * For debugging: show the BooleanFormula's in this IntTransl.
     */
    public String toString() {
	return (_isTwosComplement ? "C" : "") + Arrays.asList(_bits).toString();
    }

}
